/*! \file sroiq_language.h.
============================================================================\n
 Name        : sroiq_language.h\n
 Author      : Gergely Lukacsy (info@dlog-reasoner.org)\n
 Version     : 0.01\n
 Copyright   : DERI\n
 Description : Classes for representing SROIQ concept/role constructors,\n
               and axioms, header file.\n
 
 This file is part of the DParser and DLog 2 projects.\n
============================================================================\n

SROIQ terms defined in http://www.w3.org/TR/owl2-xml-serialization/ are mapped to the classes in this file as follows.

SROIQ Abstract Role Expressions

\code
<xsd:group name="ObjectPropertyExpression">         ---> ROLE
  <xsd:choice>
    <xsd:element ref="owl:ObjectProperty"/>         ---> ATOMICROLE
    <xsd:element ref="owl:InverseObjectProperty"/>  ---> INVERSE
  </xsd:choice>
</xsd:group>
\endcode


SROIQ Concrete Role Expressions

\code
<xsd:group name="DataPropertyExpression">           ---> ROLE
  <xsd:sequence>
    <xsd:element ref="owl:DataProperty"/>           ---> ATOMICROLE (attribute)
  </xsd:sequence>
</xsd:group>

\endcode


SROIQ Abstract Concept Expressions

\code
<xsd:group name="ClassExpression">                      ---> CONCEPT
  <xsd:choice>
    <xsd:element ref="owl:Class"/>                      ---> ATOMICCONCEPT
    <xsd:element ref="owl:ObjectIntersectionOf"/>       ---> INTERSECTION
    <xsd:element ref="owl:ObjectUnionOf"/>              ---> UNION 
    <xsd:element ref="owl:ObjectComplementOf"/>         ---> NEGATED
    <xsd:element ref="owl:ObjectOneOf"/>                ---> UNION (NOMINAL)
    <xsd:element ref="owl:ObjectSomeValuesFrom"/>       ---> EXISTS 
    <xsd:element ref="owl:ObjectAllValuesFrom"/>        ---> FORALL
    <xsd:element ref="owl:ObjectHasValue"/>             ---> EXISTS (NOMINAL)
    <xsd:element ref="owl:ObjectHasSelf"/>              ---> HASSELF
    <xsd:element ref="owl:ObjectMinCardinality"/>       ---> CARDINALITY
    <xsd:element ref="owl:ObjectMaxCardinality"/>       ---> CARDINALITY
    <xsd:element ref="owl:ObjectExactCardinality"/>     ---> CARDINALITY
    <xsd:element ref="owl:DataSomeValuesFrom"/>         ---> EXISTS (!)
    <xsd:element ref="owl:DataAllValuesFrom"/>          ---> FORALL (!)
    <xsd:element ref="owl:DataHasValue"/>               ---> EXISTS 
    <xsd:element ref="owl:DataMinCardinality"/>         ---> CARDINALITY
    <xsd:element ref="owl:DataMaxCardinality"/>         ---> CARDINALITY
    <xsd:element ref="owl:DataExactCardinality"/>       ---> CARDINALITY
  </xsd:choice>
</xsd:group>
\endcode

SROIQ Datatype Expressions

\code
<xsd:group name="DataRange">                            ---> CONCEPT
  <xsd:choice>
    <xsd:element ref="owl:Datatype"/>                   ---> ATOMICCONCEPT (attribute)
    <xsd:element ref="owl:DataIntersectionOf"/>         ---> INTERSECTION
    <xsd:e	lement ref="owl:DataUnionOf"/>              ---> UNION
    <xsd:element ref="owl:DataComplementOf"/>           ---> NEGATED
    <xsd:element ref="owl:DataOneOf"/>                  ---> UNION (NOMINAL)
    <xsd:element ref="owl:DatatypeRestriction"/>        ---> RESTRICTION
  </xsd:choice>
</xsd:group>
\endcode


SROIQ Abstract Concept Axioms

\code
<xsd:group name="ClassAxiom">
  <xsd:choice>
	<xsd:element ref="owl:SubClassOf"/>          ---> SUBCONCEPT
	<xsd:element ref="owl:EquivalentClasses"/>   ---> EQUIVALENTCONCEPTS
	<xsd:element ref="owl:DisjointClasses"/>     ---> DISJOINTCONCEPTS
	<xsd:element ref="owl:DisjointUnion"/>       ---> EQUIVALENTCONCEPTS, DISJOINTCONCEPTS
  </xsd:choice>
</xsd:group>
\endcode

SROIQ Datatype Axioms
\code
<xsd:complexType name="DatatypeDefinition">      ---> EQUIVALENTCONCEPTS
\endcode


SROIQ Abstract Role Axioms

\code
<xsd:group name="ObjectPropertyAxiom">
  <xsd:choice>
    <xsd:element ref="owl:SubObjectPropertyOf"/>                ---> SUBROLE
    <xsd:element ref="owl:EquivalentObjectProperties"/>         ---> EQUIVALENTROLES
    <xsd:element ref="owl:DisjointObjectProperties"/>           ---> DISJOINTROLES
    <xsd:element ref="owl:InverseObjectProperties"/>            ---> EQUIVALENTROLES
    <xsd:element ref="owl:ObjectPropertyDomain"/>               ---> SUBCONCEPT
    <xsd:element ref="owl:ObjectPropertyRange"/>                ---> SUBCONCEPT
    <xsd:element ref="owl:FunctionalObjectProperty"/>           ---> ATOMICROLE (attribute)
    <xsd:element ref="owl:InverseFunctionalObjectProperty"/>    ---> ATOMICROLE (attribute)
    <xsd:element ref="owl:ReflexiveObjectProperty"/>            ---> ATOMICROLE (attribute)
    <xsd:element ref="owl:IrreflexiveObjectProperty"/>          ---> ATOMICROLE (attribute)
    <xsd:element ref="owl:SymmetricObjectProperty"/>            ---> ATOMICROLE (attribute)
    <xsd:element ref="owl:AsymmetricObjectProperty"/>           ---> ATOMICROLE (attribute)
    <xsd:element ref="owl:TransitiveObjectProperty"/>           ---> ATOMICROLE (attribute)
  </xsd:choice>
</xsd:group>
\endcode

SROIQ Concrete Role Axioms

\code
<xsd:group name="DataPropertyAxiom">
  <xsd:choice>
    <xsd:element ref="owl:SubDataPropertyOf"/>          ---> SUBROLE
    <xsd:element ref="owl:EquivalentDataProperties"/>   ---> EQUIVALENTROLES
    <xsd:element ref="owl:DisjointDataProperties"/>     ---> DISJOINTROLES
    <xsd:element ref="owl:DataPropertyDomain"/>         ---> SUBCONCEPT
    <xsd:element ref="owl:DataPropertyRange"/>          ---> SUBCONCEPT
    <xsd:element ref="owl:FunctionalDataProperty"/>     ---> ATOMICROLE (attribute)
  </xsd:choice>
</xsd:group>
\endcode

SROIQ Instances

\code
<xsd:group name="Assertion">                                     ---> EXPRESSION
  <xsd:choice>
    <xsd:element ref="owl:SameIndividual"/>                      ---> SAMEINSTANCES
    <xsd:element ref="owl:DifferentIndividuals"/>                ---> DIFFERENTINSTANCES
    <xsd:element ref="owl:ClassAssertion"/>                      ---> CINSTANCE
    <xsd:element ref="owl:ObjectPropertyAssertion"/>             ---> RINSTANCE
    <xsd:element ref="owl:NegativeObjectPropertyAssertion"/>     ---> RINSTANCE (attribute)
    <xsd:element ref="owl:DataPropertyAssertion"/>               ---> RINSTANCE 
    <xsd:element ref="owl:NegativeDataPropertyAssertion"/>       ---> RINSTANCE 
  </xsd:choice>
</xsd:group>
\endcode


Other SROIQ constructs

\code
<xsd:element ref="owl:NamedIndividual"/>                ---> INSTANCE
<xsd:element ref="owl:AnonymousIndividual"/>            ---> INSTANCE
<xsd:element ref="owl:Literal"/>                        ---> INSTANCE (attribute)
<xsd:element ref="owl:HasKey"/>                         ---> HASKEY
<xsd:complexType name="FacetRestriction">               ---> FACET
<xsd:complexType name="PropertyChain">                  ---> SUBROLE
<owl:Thing>                                             ---> SROIQKB::pTOP
<owl:Nothing>                                           ---> SROIQKB::pBOTTOM
\endcode


*/

#ifndef SROIQ_LANGUAGE_H_
#define SROIQ_LANGUAGE_H_

class CONCEPT;
class ROLE;
class EXPRESSION;
class SROIQKB;
class INSTANCE;

/// Abstract class containing SROIQ terms.
/// SROIQ terms include everything, concept expressions, role expressions, individuals and axioms.
///
class SROIQTERM {
public:
	/// Virtual construction method.
	/// This method constructs (partly or fully) object \a this using a given concept.\n
	/// For example, if \a this is an existential restriction \f$ \exists R.C\f$, then given a concept, it will
	/// modify its internal state to register this concept as the concept that must hold for at-least one R follower.
	/// The default implementation of this method is empty.
	/// @param pConcept is the expression used in the construction process.
	virtual void construct(CONCEPT* pConcept);

	/// Virtual construction method.
	/// This method constructs (partly or fully) object \a this using a given role.\n
	/// For example, if \a this is an existential restriction \f$ \exists R.C\f$, then given a role, it will
	/// modify its internal state to register this role as the role on which the existential restriction holds.
	/// The default implementation of this method is empty.
	/// @param pRole is the role used in the construction process.
	virtual void construct(ROLE* pRole);

	/// Virtual construction method.
	/// This method constructs (partly or fully) object \a this using a given instance.\n
	/// For example, if \a this is an concept assertion on concept C, then given an individual, it will
	/// modify its internal state to register this instance as an instance belonging to C.
	/// The default implementation of this method is empty.
	/// @param pInstance is the instance used in the construction process.
	virtual void construct(INSTANCE* pInstance);

	/// Returns true if term is an axiom.
	virtual bool isAxiom();

	/// Returns true if term is a concept axiom.
	virtual bool isConceptAxiom();

	/// Returns true if term is a role axiom.
	virtual bool isRoleAxiom();

	/// Returns true if term is an expression.
	virtual bool isExpression();

	/// Returns true if term is an assertion.
	virtual bool isAssertion();
	
	/// Returns true if term is a concept.
	virtual bool isConcept();

	/// Returns true if term is a role.
	virtual	bool isRole();

	/// Returns true if term is a literal.
	virtual bool isLiteral();

	/// Returns true if term is a instance.
	virtual bool isInstance();

	/// Returns true if term is concrete.
	virtual bool isConcrete();

	/// Returns true if term is a facet of a literal.
	virtual bool isFacet();

	/// Returns true if term is atomic.
	virtual bool isAtomic();

	/// Returns true if term is a union.
	virtual bool isUnion();

	/// Returns true if term is an intersection.
	virtual bool isIntersection();

	/// Returns true if term is an existential restriction.
	virtual bool isExistential();

	/// Returns true if term is a universal restriction.
	virtual bool isUniversal();

	/// Returns true if term is a negation.
	virtual bool isNegated();

	/// Returns true if term is a cardinality restriction.
	virtual bool isCardinality();

	/// Returns true if term is a has self.
	virtual bool isHasSelf();

	/// Returns true if term is a nominal.
	virtual bool isNominal();

	/// Returns true if term is a datatype restriction.
	virtual bool isRestriction();

	/// Pure virtual destructor.
	virtual ~SROIQTERM() = 0;
};


/// Abstract class containing SROIQ axioms.
class AXIOM : public SROIQTERM {
public:
	/// Virtual method used for populating a knowledge base.
	/// @param kb is the knowledge base the current axiom must be inserted into
	virtual void insert(SROIQKB* pKB) = 0;

	/// Returns true if term is an axiom.
	bool isAxiom();
};

/// Abstract class containing SROIQ expressions.
/// Expressions can be concept- and role expressions.
class EXPRESSION : public SROIQTERM {
public:
	/// Virtual method used for double-dispatching.
	/// This method invokes construct() by using the following code (implemented in each subclasses)
	/// \code
	///	pGenericTerm->construct(this);
	/// \endcode
	/// @param pGenericTerm is a SROIQ term on which to invoke method construct()
	virtual void dispatchConstructInvocation(SROIQTERM* pGenericTerm) = 0;

	/// Returns true if term is an expression.
	bool isExpression();
};

/// Class representing named entities.
/// This class is not intended to be used polymorphically (no virtual destructor!).
/// The internal identifier is only accessible via getters and setters as using bit tricks we also store 4 possible states.
class NAMED {
public:
	/// Constructor.
	NAMED();

	/// Method for setting the URI of the role without managing the lifecycle of the given pointer.
	/// This method keeps the internal state of the NAMED object.
	/// @param pPrefix is a persistent external pointer.
	/// @param pName is an external pointer whose lifetime is not managed by this object.
	void setURIUnsafe(const char* pPrefix, const char* pName);

	/// Method for retrieving the URI of this atomic entity with valid pointers.
	ATOMICIDENTIFIER getURI();

	/// Retrieves the boolean value of the given named construct.
	/// @param flag is one one the constants 0x01, 0x02, 0x04... @see mProperties.
	/// @return a boolean value depending on whether the flag is set or not
	bool hasProperty(DWORD flag);

	/// Sets the given flag(s).
	/// @param key is a bitfield built up using constants 0x01, 0x02, 0x04... @see mProperties.
	void extendProperty(DWORD key);

	/// Retrieves the property field.
	/// @return the property field belonging to this object.
	DWORD getProperties();

private:
	/// Contains the URI of the given atomic role.
	ATOMICIDENTIFIER mURI;

	/// Bitfield describing the properties of the named construct.
	/// @see bTRANSITIVE, etc.
	DWORD mProperties;
};

// **********************
// SROIQ role expressions
// **********************

/// Abstract class representing roles.
class ROLE: public EXPRESSION {
public:
	/// Returns true if term is a role.
	bool isRole();
};

/// Atomic role.
class ATOMICROLE: public ROLE, public NAMED {
public:
	// We do this to avoid name hiding in this derived class.
	using ROLE::construct;

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// Constructor.
	ATOMICROLE(PARAMETERS& params);

	/// Returns true.
	bool isAtomic();

	/// Returns true if this is a datatypeProperty.
	bool isConcrete();

};

/// Class representing an inverse role.
class INVERSE : public ROLE {
public:
	friend class SUBCONCEPT;
	friend class EQUIVALENTROLES;

	// We do this to avoid name hiding in this derived class.
	using ROLE::construct;

	/// Default constructor.
	INVERSE(PARAMETERS& params);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE* pRole);

private:
	/// Internal role whose inverse this class represents.
	ROLE* pRole;
};


// **************************
// SROIQ concept expressions
// **************************


/// This is an abstract class for SROIQ concept descriptions.
class CONCEPT: public EXPRESSION {
	/// Returns true if term is a concept.
	bool isConcept();
};

/// Atomic concept.
/// State 0: abstract concept
/// State 1: concrete concept (datatype)
class ATOMICCONCEPT : public CONCEPT, public NAMED {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// Constructor.
	ATOMICCONCEPT(PARAMETERS& params);

	/// Return true if this class is a dataype entity.
	bool isConcrete();

	/// Returns true if term is atomic.
	bool isAtomic();
};

/// Class representing a nominal.
class NOMINAL : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	NOMINAL(PARAMETERS& params);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// @see SROIQTERM::construct(INSTANCE*).
	void construct(INSTANCE* pInstance);

	/// returns true if this is actually a nominal literal.
	bool isConcrete();

	/// Returns true.
	bool isNominal();


private:
	/// Internal instance.
	INSTANCE* pInstance;
};

/// Class representing a datatype restriction.
class RESTRICTION : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	RESTRICTION(PARAMETERS& params);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT* pConcept);

	/// Returns true.
	bool isRestriction();


private:
	/// Internal datatype to restrict.
	ATOMICCONCEPT* pDataType;

	/// List of facets.
	CVECTOR mFacets;
};

/// Class representing a set of literals.
/// For example the facet "0 minInclusive" represent the positive numbers.
class FACET : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	FACET(PARAMETERS& params);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// @see SROIQTERM::construct(INSTANCE*).
	void construct(INSTANCE* pInstance);

	/// Returns true.
	bool isFacet();

private:
	/// Internal literal.
	INSTANCE* pLiteral;

	/// URI of the facet identifier.
	const char* pFacetDescription;
};



/// Class representing individuals having related to themselves by a given role.
class HASSELF : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	HASSELF(PARAMETERS& params);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE* pRole);

	/// Returns true.
	bool isHasSelf();

private:
	/// Internal role of this class represents.
	ROLE* pRole;
};

/// Negated concept
class NEGATED : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	NEGATED(PARAMETERS& params): pConcept(NULL) {};

	/// Constructs a negated expression using a concept expression.
	/// @param pConcept is the concept whose negation \a this represents
	void construct(CONCEPT* pConcept);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// Returns true if this is actually a DataComplementOf
	bool isConcrete();

	/// Returns true.
	bool isNegated();

private:
	/// internal Concept whose negation this class represents.
	CONCEPT* pConcept;
};

/// Intersection of concept expressions.
class INTERSECTION : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Constructs an intersection expression using a concept expression.
	/// @param pConcept is a concept participating in the intersection \a this represents
	void construct(CONCEPT*);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// returns true if this union is actually a DataIntersectionOf
	bool isConcrete();

	/// Returns true.
	bool isIntersection();

	/// Conctructor.
	INTERSECTION(PARAMETERS& params) {}

private:
	CVECTOR mConcepts;
};

/// Union of concept expressions.
class UNION : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Constructs a union expression using a concept expression.
	/// @param pConcept is a concept participating in the union \a this represents
	void construct(CONCEPT* pConcept);

	/// Constructs a union expression using an instance.
	/// @param pInstance is an instance participating in the union \a this represents
	void construct(INSTANCE* pInstance);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// returns true if this union is actually a DataUnionOf
	bool isConcrete();

	/// Returns true.
	bool isUnion();

	/// Constructor.
	UNION(PARAMETERS& params);
private:

	/// List of concepts whose union this object represents.
	CVECTOR mConcepts;
};

/// Value restriction.
/// Describes concepts of the form \f$\forall R.C\f$, where R is a role and C is a concept.
/// All individuals belong to this concept whose R followers all belong to C.
///
/// Examples:
///
/// \f$\forall \textit{hasChild}.\textit{Clever}\f$\n
/// \f$\forall \textit{hasWife}.\textit{Clever} \sqcup \textit{Beautiful}\f$
class FORALL : public CONCEPT {
public:
	friend class SUBCONCEPT;

	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	FORALL(PARAMETERS& params): pRole(NULL), pConcept(NULL) {}

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE*);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// Returns true.
	bool isUniversal();

private:
	/// Role of the value restriction.
	ROLE* pRole;

	/// Concept of the value restriction.
	CONCEPT* pConcept;
};

/// Existential restriction.
/// Describes concepts of the form \f$\exists R.C\f$, where R is a role and C is a concept (including nominals).
/// All individuals belong to this concept having at-least one R follower belonging to C.
///
/// Examples:
///
/// \f$\exists \textit{hasChild}.\textit{Clever}\f$\n
/// \f$\exists \textit{hasWife}.\textit{Clever} \sqcup \textit{Beautiful}\f$
/// \f$\exists \textit{hasChild}.\textit{\{JOHN\}}\f$\n
class EXISTS : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	EXISTS(PARAMETERS& params): pRole(NULL), pConcept(NULL) {}

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE*);

	/// @see SROIQTERM::construct(INSTANCE*).
	void construct(INSTANCE*);

	/// Returns true.
	bool isExistential();

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

private:
	/// Role on which the existential restriction holds.
	ROLE* pRole;

	/// The concept of the existential restriction.
	CONCEPT* pConcept;
};


/// Qualified number restriction (at-least, at-most, exact).
class CARDINALITY : public CONCEPT {
public:
	// We do this to avoid name hiding in this derived class.
	using CONCEPT::construct;

	/// Default constructor.
	CARDINALITY(PARAMETERS& params);

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE*);

	/// Returns true.
	bool isCardinality();

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

private:

	/// The role on which we put a cardinality restriction.
	ROLE* pRole;

	/// The concept of the cardinality restriction.
	CONCEPT* pConcept;

	/// The cardinality itself.
	unsigned nCardinality : 30;

	/// Type of the cardinality restriction.
	/// valMINCARDINALITY - AT-LEAST\n
	/// valMAXCARDINALITY - AT-MOST\n
	/// valEXACTCARDINALITY - EXACT\n
	unsigned mType : 2;
};


//**********
// Instances
//**********

/// SROIQ assertions.
class ASSERTION: public AXIOM {
	/// Returns true if term is an assertion.
	bool isAssertion();
};

/// An SROIQ instance (literal).
class INSTANCE: public EXPRESSION, public NAMED {
public:
	/// Constructor.
	INSTANCE(PARAMETERS&);

	/// Method for double-dispatching.
	void dispatchConstructInvocation(SROIQTERM*);

	/// Returns true.
	bool isInstance();

	/// Returns true if this instance is a literal .
	bool isLiteral();

	/// Returns true if this instance is a literal.
	bool isConcrete();

	/// Returns true.
	bool isAtomic();
};


/// Concept assertion.
/// For example, Patricide(Oedipus)
class CINSTANCE: public ASSERTION {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// Constructor.
	CINSTANCE(PARAMETERS& params);

	/// @see SROIQTERM::construct(INSTANCE*).
	void construct(INSTANCE*);

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

private:

	/// Concept to which instance pInstance belongs to.
	CONCEPT* pConcept;

	/// The instance who belongs to pConcept.
	INSTANCE* pInstance;
};

/// Role assertion.
/// For example, hasChild(Iocaste, Oedipus)
class RINSTANCE: public ASSERTION {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// Constructor.
	RINSTANCE(PARAMETERS& params);

	/// @see SROIQTERM::construct(INSTANCE*).
	void construct(INSTANCE*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

private:

	/// The role that holds between pInstanceSource and pInstanceTarget.
	ROLE* pRole;

	/// Instance on the left.
	INSTANCE* pInstanceSource;

	/// Instance on the right.
	INSTANCE* pInstanceTarget;

	/// Type of the role assertion (positive, negative).
	ASSTYPES mType;
};

/// Assertion on same individuals.
class SAMEINSTANCES: public ASSERTION {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// Constructor.
	SAMEINSTANCES(PARAMETERS&);

	/// @see SROIQTERM::construct(INSTANCE*).
	void construct(INSTANCE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

private:

	/// List of instance names which denote the same instance.
	IVECTOR mInstances;
};

/// Assertion on different individuals.
class DIFFERENTINSTANCES: public ASSERTION {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// Constructor.
	DIFFERENTINSTANCES(PARAMETERS&);

	/// @see SROIQTERM::construct(INSTANCE*).
	void construct(INSTANCE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

private:

	/// List of instance names that denote different instances. 
	IVECTOR mInstances;
};

// ******
// axioms
// ******


/// SROIQ role axioms.
class ROLEAXIOM: public AXIOM {
	/// Returns true if term is a role axiom.
	bool isRoleAxiom();
};

/// SROIQ concept axioms.
class CONCEPTAXIOM: public AXIOM {
	/// Returns true if term is a concept axiom.
	bool isConceptAxiom();
};

/// SROIQ key axiom.
class HASKEY: public AXIOM {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// Constructor.
	HASKEY(PARAMETERS& params);

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

private:
	/// The concept whose instance are uniquely identified by mObjectProperties or mDataTypeProperties.
	CONCEPT* pConcept;

	/// Complex key.
	RVECTOR mObjectProperties;

	/// Complex key.
	RVECTOR mDataTypeProperties;
};


/// Concept subsumption axiom.
/// This class is used to describe axioms of the form:
///
/// \f$ C_1 \sqsubseteq C_2\f$
///
/// Specially we use such axioms to represent domain and range restrictions on roles.
class SUBCONCEPT: public CONCEPTAXIOM {
public:
	friend class OWLHANDLER;

	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// Constructor.
	SUBCONCEPT(PARAMETERS& params);

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

private:
	/// Concept expression on the left hand side.
	CONCEPT* pLeftConcept;

	/// Concept expression on the right hand side.
	CONCEPT* pRightConcept;

	/// Origin of this axiom.
	SUBTYPES mOrigin;

};


/// Concept equivalence axiom.
/// Also used as part of a DisjointUnionOf axiom.
class EQUIVALENTCONCEPTS: public CONCEPTAXIOM {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

	/// Constructor.
	EQUIVALENTCONCEPTS(PARAMETERS& params);

private:

	/// Concept vector holding the equivalent concepts.
	CVECTOR mConcepts;

	/// Origin info
	EQTYPES mOrigin;

};

/// Concept disjoint axiom.
class DISJOINTCONCEPTS: public CONCEPTAXIOM {
public:
	friend class EQUIVALENTCONCEPTS;

	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(CONCEPT*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

	/// Constructor.
	DISJOINTCONCEPTS(PARAMETERS& params) {}

private:

	/// Concept vector holding the disjoint concepts.
	CVECTOR mConcepts;
};


/// Role subsmuption axiom.
class SUBROLE: public ROLEAXIOM {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// Default constructor.
	SUBROLE(PARAMETERS& params):
		pRightRole(NULL)	{}

	/// @see SROIQTERM::construct(ROLE*).
	void construct(ROLE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

private:
	/// More than one roles can be on the left side because of property chains.
	RVECTOR mLeftRoles;

	/// The right hand side of the subrole axiom.
	ROLE* pRightRole;
};

/// Role equivalence axiom.
/// As a special case it is used for storing the fact that R = inv(S).
class EQUIVALENTROLES: public ROLEAXIOM {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(ROLE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

	/// Constructor.
	EQUIVALENTROLES(PARAMETERS& params);

private:
	/// Role vector holding the equivalent roles.
	RVECTOR mRoles;

	/// Origin info
	ERTYPES mOrigin;
};

/// Role disjointness axiom.
class DISJOINTROLES: public ROLEAXIOM {
public:
	// We do this to avoid name hiding in this derived class.
	using AXIOM::construct;

	/// @see SROIQTERM::construct(CONCEPT*).
	void construct(ROLE*);

	/// Insertion method.
	void insert(SROIQKB* pKB);

	/// Constructor.
	DISJOINTROLES(PARAMETERS& params) {}

private:

	/// Role vector holding the equivalent roles.
	RVECTOR mRoles;
};

// ********************
// SROIQ knowledge base
// ********************

/// Describes a TBox.
/// A TBox contains generic concept subsumption and equivalence axioms
class TBOX {
public:
	/// Concept subsumtion axioms.
	SCVECTOR mSubsumptionAxioms;

	/// Concept equivalence axioms.
	ECVECTOR mEquivalenceAxioms;

	/// Concept disjoint axioms.
	DCVECTOR mDisjointAxioms;

	/// HasKey axioms.
	KVECTOR  mKeys;
};

/// Describes and RBox.
/// An RBox contains generic role subsumption axioms and transitivity axioms
class RBOX {
public:

	/// Role subsumption axioms.
	SRVECTOR mSubsumptionAxioms;

	/// Role equivalence axioms.
	ERVECTOR mEquivalenceAxioms;

	/// Role disjoint axioms.
	DRVECTOR mDisjointAxioms;
};

/// Describes an ABox.
///  An ABox contains facts about individuals (concept and role assertions)
class ABOX {
public:
	
	/// Concept assertions.
	CINSTANCEVECTOR mConceptAssertions;

	/// Role assertions.
	RINSTANCEVECTOR mRoleAssertions;
	
	/// Equivalent instances.
	SIVECTOR mSameInstances;

	/// Different instances.
	DIVECTOR mDifferentInstances;
};


/// Compares two atomic construct based on their URIs.
struct ATOMICCOMPARE : public std::binary_function<NAMED*, NAMED*, bool> {
  bool operator() (NAMED* a1, NAMED* a2) const {
	  ASSERT(a1 != NULL);
	  ASSERT(a2 != NULL);
	  const char* pLocal1 = a1->getURI().pLocalName;
	  const char* pLocal2 = a2->getURI().pLocalName;
	  ASSERT(pLocal1 != NULL);
	  ASSERT(pLocal2 != NULL);

	  // simply iterate through the virtual concatenation of pPrefix1+pLocal1 and pPrefix2+pLocal2 and compare
	  const char* src = a1->getURI().pPrefix;
	  const char* dst = a2->getURI().pPrefix;
	  bool bSrcFirst = true;
	  bool bDstFirst = true;

	  ASSERT(src != NULL); // ???
	  ASSERT(dst != NULL); // ???

	  while ((*src && *dst) || (bSrcFirst || bDstFirst)) {
		  // If we reached the end of prefix1 continue with localname1
		  if ((*src == 0) && (bSrcFirst)) {
			  src = pLocal1;
			  bSrcFirst = false;
		  }

		  // If we reached the end of prefix2 continue with localname2
		  if ((*dst == 0) && (bDstFirst)) {
			  dst = pLocal2;
			  bDstFirst = false;
		  }

		  // compare characters
		  INT diff = *(unsigned char *)src - *(unsigned char *)dst;

		  // we return if there is any difference
		  if (diff != 0)
			  return false;

		  ASSERT(*src);
		  ASSERT(*dst);

		  // step forward
          ++src;
          ++dst;
	  }

	  return true;
  }
};

/// A class that can calculate a hash value for an ATOMICIDENTIFIER type
/// The following is the SGI hash template specialisation for char*.
/// \code
///inline size_t __stl_hash_string(const char* __s)
///{
///  unsigned long __h = 0;
///  for ( ; *__s; ++__s)
///    __h = 5*__h + *__s;
///
///  return size_t(__h);
///}
/// \endcode
struct ATOMICHASH {
	static size_t hash(ATOMICIDENTIFIER mId) {
		ASSERT(mId.pPrefix != NULL);
		ASSERT(mId.pLocalName != NULL);

		const char* __s = mId.pPrefix;

		// hash first part of the absolute URI
		unsigned long __h = 0;
		for ( ; *__s; ++__s)
			__h = 5*__h + *__s;

		// hash the second part
		__s = mId.pLocalName;
		for ( ; *__s; ++__s)
			__h = 5*__h + *__s;

		// return hash value
		return size_t(__h);
	}
};

struct I_CONCEPTTABLE;
struct I_ROLETABLE;
struct I_INSTANCETABLE;

/// Describes a Description Logic knowledge base.
/// A Knowledge Base consists an atom table storing the URIs of the atomic classes/roles and individuals. It also consists of an
/// - TBox\n
/// - RBox\n
/// - ABox\n
class SROIQKB {
public:
	/// The TBox.
	TBOX mTBox;

	/// The RBox.
	RBOX mRBox;

	/// The ABox.
	ABOX mABox;

	/// Method to add a new element to the concept table.
	/// This method extends the concept table with an element if it has been not there previously.
	/// @param pNewAtomicConcept is the concept to add.
	/// @return A persistent pointer to the element referenced in the concept table.
	ATOMICCONCEPT* addAtomic(ATOMICCONCEPT* pNewAtomicConcept);

	/// Method to add a new element to the role table.
	/// This method extends the role table with an element if it has been not there previously.
	/// @param pNewAtomicRole is the role to add.
	/// @return A persistent pointer to the element referenced in the role table.
	ATOMICROLE* addAtomic(ATOMICROLE* pNewAtomicRole);

	/// Method to add a new element to the instance table.
	/// This method extends the instance table with an element if it has been not there previously.
	/// @param pNewInstance is the instance to add.
	/// @return A persistent pointer to the element referenced in the instance table.
	INSTANCE* addAtomic(INSTANCE* pNewInstance);

	/// Constructor.
	SROIQKB();

	/// Destructor.
	~SROIQKB();

	/// Block allocator for efficient small object creation.
	BLOCKALLOCATOR mPool;

	/// Singleton object for TOP.
	ATOMICCONCEPT* pTOP;

	/// Singleton object for BOTTOM.
	ATOMICCONCEPT* pBOTTOM;

private:
	/// Table for storing atomic concepts.
	I_CONCEPTTABLE* pConceptTable;

	/// Table for storing atomic roles.
	I_ROLETABLE* pRoleTable;

	/// Table for storing instances.
	I_INSTANCETABLE* pInstanceTable;

	/// Template for adding an element to one of the tables;
	template <typename A, typename T>
	A* _addAtomic(A* pNewElement, T& mTable);

	/// Number of objects that are allocated as one unit.
	static const INT nrGrouppedObjects;
};


#endif /* SROIQ_LANGUAGE_H_ */
